Nuprl Lemma : zip_wf
11,40
postcript
pdf
T1
,
T2
:Type,
as
:(
T1
List),
bs
:(
T2
List). zip(
as
;
bs
)
((
:
T1
T2
) List)
latex
ProofTree
Definitions
Y
,
zip(
as
;
bs
)
,
t
T
,
x
:
A
.
B
(
x
)
,
{
T
}
Lemmas
member
wf
origin
T1, T2:Type, as:(T1 List), bs:(T2 List). zip(as;bs) 
((:T1 
T2) List)
T1, T2:Type, as:(T1 List), bs:(T2 List). zip(as;bs) ((:T1 T2) List)
Tx:A. B(x)